These are archival webpages, generated on 2023-03-20 by Prove-It Beta Version 0.3, licensed under the GNU Public Licence by Sandia Corporation. See pyproveit.org for the lastest version.
logo
In [1]:
import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
    Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
    QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
    _s, _t, _ket_u, _U, _phase,
    _s_in_nat_pos, _u_ket_register, _normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
    QPE1_def, _psi_t_def, _psi_t_ket_register)
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving _psi_t_output
Out[2]:
Under these presumptions, we begin our proof of
_psi_t_output:
(see dependencies)
In [3]:
_psi_t_output
Out[3]:
In [4]:
defaults.assumptions = _psi_t_output.conditions
Out[4]:
defaults.assumptions:
In [ ]:
 

We should automate the following so it isn't necessary.

In [5]:
_s_in_nat_pos
Out[5]:
In [6]:
from proveit.logic import InSet
from proveit.numbers import Natural, greater, greater_eq, zero, Neg
In [7]:
# greater_eq(_s, one).prove().derive_shifted(Neg(one))
In [8]:
# InSet(subtract(_s, one), Natural).prove()
In [9]:
# greater_eq(t, one).prove().derive_shifted(Neg(one))
In [10]:
tm1_in_N = InSet(subtract(t, one), Natural).prove()
Out[10]:
tm1_in_N:  ⊢  
In [11]:
tm1_in_N.inner_expr().element.commute()
Out[11]:
In [ ]:
 
In [12]:
_psi_t_def
Out[12]:
In [13]:
_psi_t = _psi_t_def.instantiate()
Out[13]:
_psi_t:  ⊢  
In [14]:
_psi_t_ket_register
Out[14]:
In [15]:
_psi_t_ket_register.instantiate()
Out[15]:
In [ ]:
 
In [16]:
from proveit.logic import CartExp
from proveit.numbers import Complex
In [17]:
#InSet(_psi_t.rhs, CartExp(Complex, Exp(two, t))).prove()
In [18]:
from proveit import r
from proveit.numbers import NaturalPos
InSet(_psi_t.rhs.operands[0].body, CartExp(Complex, two)).prove(assumptions=[InSet(r, NaturalPos)])
Out[18]:
In [19]:
InSet(_psi_t.rhs.operands[0].body, CartExp(Complex, Exp(two, one))).prove(assumptions=[InSet(r, NaturalPos)])
Out[19]:
In [20]:
# InSet(_psi_t.rhs.operands[0].body.scaled, CartExp(Complex, two)).prove(assumptions=[InSet(r, NaturalPos)])
In [21]:
# from proveit.linear_algebra import TensorProd
# InSet(TensorProd(_psi_t.rhs.operands[0].body, _psi_t.rhs.operands[0].body), CartExp(Complex, Exp(two, two))).prove()
In [ ]:
 
In [22]:
target_circuit = _psi_t_output.instance_expr.lhs.operand
Out[22]:
target_circuit:
In [23]:
QPE1_def
Out[23]:
In [24]:
QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})
Out[24]:
QPE1_inst:  ⊢  
In [25]:
phase_kickbacks_on_register
Out[25]:
In [26]:
Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)), 
                                    subtract(t, one), zero, order='decreasing'))
Out[26]:
Uexponentials:
In [ ]:
 

We should automate the following so it isn't necessary.

In [27]:
Neg(subtract(t, one)).simplification()
Out[27]:
In [28]:
t_gt_0 = greater(t, zero).prove()
Out[28]:
t_gt_0:  ⊢  
In [29]:
from proveit.numbers import Less
Less(Neg(one), zero).prove()
Out[29]:
In [30]:
nt_lt_0 = t_gt_0.left_mult_both_sides(Neg(one))
Out[30]:
nt_lt_0:  ⊢  
In [31]:
nt_lt_0.derive_shifted(one)
Out[31]:
In [32]:
t_geq_1 = greater_eq(t, one).prove()
Out[32]:
t_geq_1:  ⊢  
In [33]:
nt_leq_1 = t_geq_1.left_mult_both_sides(Neg(one))
Out[33]:
nt_leq_1:  ⊢  
In [34]:
nt_leq_1.derive_shifted(two)
Out[34]:
In [35]:
nt_lt_0.derive_shifted(one)
Out[35]:
In [36]:
from proveit.numbers import Add
Add(t, one).commutation()
Out[36]:
In [37]:
Add(t, two).commutation()
Out[37]:
In [38]:
from proveit.numbers import Interval
tmp_assumptions = defaults.assumptions+(InSet(k, Interval(Add(Neg(t), one), zero)),)
k_gt_ntp1 = greater_eq(k, Add(Neg(t), one)).prove(
    assumptions=tmp_assumptions)
Out[38]:
k_gt_ntp1: ,  ⊢  
In [39]:
from proveit.numbers import Integer
Add(k, t).deduce_bound(k_gt_ntp1, assumptions=tmp_assumptions)
Out[39]:
In [40]:
greater(Add(k, t), zero).prove(assumptions=tmp_assumptions)
Out[40]:
In [41]:
InSet(Add(k, t), Integer).prove(assumptions=tmp_assumptions)
Out[41]:
In [42]:
InSet(Add(k, t), Natural).prove(assumptions=tmp_assumptions).generalize(
    k, conditions=[InSet(k, Interval(Add(Neg(t), one), zero))])
Out[42]:
In [43]:
subtract(one, Add(Neg(t), two)).simplification()
Out[43]:
In [ ]:
 
In [44]:
from proveit.logic import And, InSet
And(ExprRange(k, InSet(MatrixExp(_U, Exp(two, k)), _unitary_U.domain), 
                                    subtract(t, one), zero, order='decreasing')).conclude_over_expr_range()
Out[44]:
In [45]:
phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase), 
                             subtract(t, one), zero, order='decreasing'))
Out[45]:
phases:
In [ ]:
 
In [46]:
kickbacks = phase_kickbacks_on_register.instantiate(
    {m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})
Out[46]:
kickbacks:  ⊢  
In [47]:
kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
    kickbacks.inner_expr().lhs.operand)
Out[47]:
kickbacks_with_QPE1:  ⊢  

For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:

In [48]:
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex
Out[48]:
VecSpaces.default_field:
In [49]:
psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))
Out[49]:
psi_t_tensor_u__expansion:  ⊢  
In [ ]:
 

We should automate the following so it isn't necessary.

In [50]:
from proveit._core_.expression.label.var import dummy_var
assumptions = defaults.assumptions + (InSet(dummy_var(0), Interval(Add(Neg(t), one), zero)),)
Out[50]:
assumptions:
In [51]:
Add(dummy_var(0), t).deduce_bound(assumptions[1].derive_element_lower_bound(
   assumptions=assumptions).reversed(), assumptions=assumptions)
Out[51]:
In [52]:
Add(dummy_var(0), t).deduce_in_number_set(NaturalPos, assumptions=assumptions)
Out[52]:
In [ ]:
 
In [53]:
output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
    replacements=[psi_t_tensor_u__expansion.derive_reversed()])
Out[53]:
output_consolidation:  ⊢  
In [54]:
output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()
Out[54]:
output_consolidation_from_desired:  ⊢  
In [55]:
equiv = output_consolidation.apply_transitivity(
    output_consolidation_from_desired, assumptions=defaults.assumptions + (InSet(_psi_t.rhs, CartExp(Complex, Exp(two, t))),))
Out[55]:
equiv:  ⊢  
In [56]:
equiv.sub_right_side_into(kickbacks_with_QPE1)
Out[56]:
In [57]:
%qed
Out[57]:
 step typerequirementsstatement
0generalization1  ⊢  
1instantiation4, 2, 3  ⊢  
  : , : , :
2instantiation4, 5, 6  ⊢  
  : , : , :
3instantiation7, 8, 9  ⊢  
  : , : , :
4conjecture  ⊢  
 proveit.physics.quantum.circuits.rhs_prob_via_equiv
5instantiation10, 494, 689, 11, 12, 338, 13, 14, 15, 680, 656, 16, 17*  ⊢  
  : , : , : , : , :
6modus ponens18, 19  ⊢  
7conjecture  ⊢  
 proveit.physics.quantum.circuits.equiv_transitivity
8modus ponens20, 21  ⊢  
9instantiation34, 22  ⊢  
  : , :
10conjecture  ⊢  
 proveit.physics.quantum.circuits.phase_kickbacks_on_register
11instantiation584, 23, 467  ⊢  
  : , : , :
12modus ponens24, 25  ⊢  
13axiom  ⊢  
 proveit.physics.quantum.QPE._normalized_ket_u
14instantiation584, 26, 467  ⊢  
  : , : , :
15modus ponens27, 28  ⊢  
16instantiation263, 679, 264, 75, 76, 77*  ⊢  
  : , : , : , : , : , :
17instantiation29, 614, 664, 682, 30, 31, 615, 602, 594, 595, 32, 597,  ⊢  
  : , : , : , : , : , :
18instantiation51, 610, 527, 33  ⊢  
  : , : , : , : , : , : , : , :
19instantiation34, 35  ⊢  
  : , :
20instantiation51, 664, 610, 682, 52, 615  ⊢  
  : , : , : , : , : , : , : , :
21instantiation578, 36, 37  ⊢  
  : , : , :
22modus ponens38, 39  ⊢  
23instantiation578, 40, 528  ⊢  
  : , : , :
24instantiation471, 676, 677, 472  ⊢  
  : , : , : , :
25generalization41  ⊢  
26instantiation578, 42, 528  ⊢  
  : , : , :
27instantiation471, 676, 677, 472  ⊢  
  : , : , : , :
28generalization43  ⊢  
29conjecture  ⊢  
 proveit.numbers.multiplication.disassociation
30instantiation632  ⊢  
  : , : , :
31instantiation631  ⊢  
  : , :
32instantiation685, 635, 44,  ⊢  
  : , : , :
33instantiation584, 45, 467  ⊢  
  : , : , :
34conjecture  ⊢  
 proveit.physics.quantum.circuits.equiv_reflexivity
35instantiation46, 494, 689, 64  ⊢  
  : , : , :
36instantiation578, 47, 48  ⊢  
  : , : , :
37instantiation238, 527, 72, 49, 50  ⊢  
  : , : , : , :
38instantiation51, 664, 610, 682, 52, 615  ⊢  
  : , : , : , : , : , : , : , :
39instantiation89, 666, 53, 689, 494, 54, 55, 338, 56, 57, 58, 59, 60, 579, 417, 682, 527, 103, 61, 605*  ⊢  
  : , : , : , : , : , :
40instantiation508, 509  ⊢  
  : , : , :
41instantiation62, 63, 435, 64,  ⊢  
  : , : , :
42instantiation508, 509  ⊢  
  : , : , :
43instantiation65, 123, 627, 66,  ⊢  
  : , : , : , :
44instantiation685, 652, 67,  ⊢  
  : , : , :
45instantiation578, 68, 528  ⊢  
  : , : , :
46axiom  ⊢  
 proveit.physics.quantum.QPE.QPE1_def
47instantiation578, 69, 70  ⊢  
  : , : , :
48instantiation238, 527, 71, 72, 73  ⊢  
  : , : , : , :
49instantiation74, 527  ⊢  
  : , :
50instantiation263, 679, 264, 75, 76, 77*  ⊢  
  : , : , : , : , : , :
51conjecture  ⊢  
 proveit.physics.quantum.circuits.circuit_equiv_temporal_sub
52instantiation631  ⊢  
  : , :
53instantiation631  ⊢  
  : , :
54instantiation631  ⊢  
  : , :
55instantiation78, 689  ⊢  
  :
56instantiation584, 79, 80  ⊢  
  : , : , :
57instantiation492, 81  ⊢  
  : , :
58instantiation631  ⊢  
  : , :
59instantiation492, 82  ⊢  
  : , :
60instantiation584, 83, 84  ⊢  
  : , : , :
61instantiation186, 614, 85, 189, 86, 192  ⊢  
  : , :
62conjecture  ⊢  
 proveit.linear_algebra.matrices.exponentiation.U_closure
63instantiation663, 664, 87,  ⊢  
  : , :
64axiom  ⊢  
 proveit.physics.quantum.QPE._unitary_U
65conjecture  ⊢  
 proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application
66axiom  ⊢  
 proveit.physics.quantum.QPE._eigen_uu
67instantiation685, 655, 88,  ⊢  
  : , : , :
68instantiation508, 509  ⊢  
  : , : , :
69instantiation89, 364, 90, 687, 91, 494, 92, 93, 94, 338, 95, 96, 97, 98, 99, 100, 101, 579, 176, 682, 102, 103, 104, 605, 327*, 105*, 106*  ⊢  
  : , : , : , : , : , :
70instantiation238, 527, 107, 108, 109, 110*  ⊢  
  : , : , : , :
71instantiation584, 111, 467  ⊢  
  : , : , :
72instantiation584, 112, 467  ⊢  
  : , : , :
73instantiation282, 283, 284, 371*  ⊢  
  : , : , : , :
74conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len_typical_eq
75instantiation492, 113  ⊢  
  : , :
76instantiation492, 114  ⊢  
  : , :
77instantiation584, 115, 116,  ⊢  
  : , : , :
78conjecture  ⊢  
 proveit.physics.quantum.QPE._psi_t_ket_register
79instantiation117  ⊢  
  : , : , :
80instantiation492, 118  ⊢  
  : , :
81instantiation218, 119, 605  ⊢  
  : , : , :
82instantiation270, 119, 417  ⊢  
  : , : , :
83instantiation120  ⊢  
  : , :
84instantiation492, 121  ⊢  
  : , :
85instantiation632  ⊢  
  : , : , :
86instantiation492, 481  ⊢  
  : , :
87instantiation667, 122,  ⊢  
  :
88instantiation685, 686, 123,  ⊢  
  : , : , :
89conjecture  ⊢  
 proveit.physics.quantum.circuits.output_consolidation
90instantiation584, 124, 134  ⊢  
  : , : , :
91instantiation468, 654, 677, 687, 279  ⊢  
  : , : , :
92instantiation584, 125, 134  ⊢  
  : , : , :
93instantiation526, 126, 209  ⊢  
  : , : , :
94modus ponens127, 128  ⊢  
95instantiation584, 129, 130  ⊢  
  : , : , :
96instantiation492, 131  ⊢  
  : , :
97instantiation492, 132  ⊢  
  : , :
98instantiation584, 133, 134  ⊢  
  : , : , :
99instantiation492, 135  ⊢  
  : , :
100instantiation492, 136  ⊢  
  : , :
101instantiation584, 137, 138  ⊢  
  : , : , :
102modus ponens139, 140  ⊢  
103instantiation685, 543, 141  ⊢  
  : , : , :
104instantiation142, 664, 358, 610, 143, 426, 144, 145  ⊢  
  : , : , : , : , : , :
105instantiation584, 146, 147  ⊢  
  : , : , :
106instantiation584, 148, 198  ⊢  
  : , : , :
107instantiation584, 149, 467  ⊢  
  : , : , :
108instantiation584, 150, 467  ⊢  
  : , : , :
109instantiation282, 283, 284, 151*  ⊢  
  : , : , : , :
110instantiation245, 152,  ⊢  
  : , :
111instantiation328, 666, 153, 330, 344, 331, 358, 332*  ⊢  
  : , : , : , :
112instantiation578, 154, 528  ⊢  
  : , : , :
113instantiation584, 155, 371  ⊢  
  : , : , :
114instantiation584, 156, 481  ⊢  
  : , : , :
115instantiation609, 682, 664, 610, 615, 157, 158, 582, 617,  ⊢  
  : , : , : , : , : , :
116instantiation587, 617, 158,  ⊢  
  : , :
117conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3
118instantiation578, 159, 248  ⊢  
  : , : , :
119instantiation526, 664, 160  ⊢  
  : , : , :
120conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2
121instantiation578, 161, 249  ⊢  
  : , : , :
122instantiation669, 453, 162,  ⊢  
  :
123instantiation663, 664, 163,  ⊢  
  : , :
124instantiation328, 210, 164, 180, 213, 331, 358, 181*  ⊢  
  : , : , : , :
125instantiation328, 210, 165, 180, 213, 331, 358, 181*  ⊢  
  : , : , : , :
126instantiation532, 533, 496, 166  ⊢  
  : , : , : , :
127instantiation471, 654, 677, 279  ⊢  
  : , : , : , :
128generalization167  ⊢  
129instantiation584, 168, 169  ⊢  
  : , : , :
130instantiation492, 170  ⊢  
  : , :
131instantiation218, 175, 605  ⊢  
  : , : , :
132instantiation238, 527, 222, 171, 172  ⊢  
  : , : , : , :
133instantiation328, 210, 173, 180, 213, 331, 358, 181*  ⊢  
  : , : , : , :
134instantiation492, 174  ⊢  
  : , :
135instantiation270, 175, 176  ⊢  
  : , : , :
136instantiation584, 177, 178  ⊢  
  : , : , :
137instantiation328, 210, 179, 180, 213, 331, 358, 181*  ⊢  
  : , : , : , :
138instantiation492, 182  ⊢  
  : , :
139instantiation471, 676, 677, 472  ⊢  
  : , : , : , :
140generalization183  ⊢  
141instantiation406, 689, 494  ⊢  
  : , :
142conjecture  ⊢  
 proveit.logic.booleans.conjunction.disassociate
143instantiation631  ⊢  
  : , :
144instantiation584, 184, 185  ⊢  
  : , : , :
145instantiation186, 187, 188, 189, 190, 191, 192  ⊢  
  : , :
146instantiation576, 193  ⊢  
  : , : , :
147instantiation492, 194  ⊢  
  : , :
148instantiation576, 605  ⊢  
  : , : , :
149instantiation328, 666, 195, 330, 344, 331, 358, 332*  ⊢  
  : , : , : , :
150instantiation578, 196, 528  ⊢  
  : , : , :
151instantiation584, 197, 198  ⊢  
  : , : , :
152instantiation199, 200, 201,  ⊢  
  :
153instantiation631  ⊢  
  : , :
154instantiation508, 509  ⊢  
  : , : , :
155instantiation576, 583  ⊢  
  : , : , :
156instantiation576, 583  ⊢  
  : , : , :
157instantiation631  ⊢  
  : , :
158instantiation685, 635, 202,  ⊢  
  : , : , :
159instantiation508, 203  ⊢  
  : , : , :
160instantiation584, 204, 439  ⊢  
  : , : , :
161instantiation508, 205  ⊢  
  : , : , :
162instantiation673, 676, 677, 483,  ⊢  
  : , : , :
163instantiation667, 206,  ⊢  
  :
164instantiation632  ⊢  
  : , : , :
165instantiation632  ⊢  
  : , : , :
166instantiation514, 533, 515, 207  ⊢  
  : , : , : , :
167instantiation526, 208, 209,  ⊢  
  : , : , :
168instantiation328, 210, 211, 212, 213, 331, 509, 214*  ⊢  
  : , : , : , :
169instantiation492, 215  ⊢  
  : , :
170instantiation578, 216, 304  ⊢  
  : , : , :
171instantiation584, 217, 467  ⊢  
  : , : , :
172instantiation218, 283, 353, 371*  ⊢  
  : , : , :
173instantiation632  ⊢  
  : , : , :
174instantiation510, 321  ⊢  
  : , :
175instantiation526, 321, 219  ⊢  
  : , : , :
176instantiation584, 220, 221  ⊢  
  : , : , :
177instantiation238, 527, 222, 224, 223  ⊢  
  : , : , : , :
178instantiation238, 527, 224, 225, 226  ⊢  
  : , : , : , :
179instantiation632  ⊢  
  : , : , :
180instantiation632  ⊢  
  : , : , :
181instantiation584, 227, 228  ⊢  
  : , : , :
182instantiation578, 229, 322  ⊢  
  : , : , :
183instantiation553, 230, 231,  ⊢  
  :
184instantiation578, 232, 426  ⊢  
  : , : , :
185instantiation492, 233  ⊢  
  : , :
186conjecture  ⊢  
 proveit.logic.booleans.conjunction.and_if_all
187conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat4
188instantiation234  ⊢  
  : , : , : , :
189instantiation237  ⊢  
  :
190instantiation492, 605  ⊢  
  : , :
191modus ponens235, 236  ⊢  
192instantiation237  ⊢  
  :
193instantiation238, 527, 239, 385, 240  ⊢  
  : , : , : , :
194instantiation576, 241, 242*  ⊢  
  : , : , :
195instantiation631  ⊢  
  : , :
196instantiation508, 509  ⊢  
  : , : , :
197instantiation422, 614, 243, 244, 371, 562  ⊢  
  : , : , : , :
198instantiation245, 687  ⊢  
  : , :
199conjecture  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
200instantiation678, 670, 656,  ⊢  
  : , :
201instantiation323, 324, 246,  ⊢  
  : , : , :
202instantiation685, 652, 247,  ⊢  
  : , : , :
203instantiation526, 614, 248  ⊢  
  : , : , :
204instantiation576, 407  ⊢  
  : , : , :
205instantiation526, 664, 249  ⊢  
  : , : , :
206instantiation669, 250, 251,  ⊢  
  :
207instantiation532, 533, 252, 535  ⊢  
  : , : , : , :
208instantiation532, 533, 496, 253,  ⊢  
  : , : , : , :
209instantiation576, 254  ⊢  
  : , : , :
210conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat3
211instantiation632  ⊢  
  : , : , :
212instantiation632  ⊢  
  : , : , :
213instantiation632  ⊢  
  : , : , :
214instantiation584, 255, 256  ⊢  
  : , : , :
215instantiation606, 617, 602  ⊢  
  : , :
216instantiation508, 257  ⊢  
  : , : , :
217instantiation328, 666, 258, 330, 344, 331, 358, 332*  ⊢  
  : , : , : , :
218conjecture  ⊢  
 proveit.core_expr_types.tuples.partition_front
219instantiation584, 259, 260  ⊢  
  : , : , :
220instantiation609, 682, 664, 610, 615, 477, 617, 619, 618  ⊢  
  : , : , : , : , : , :
221instantiation261, 619, 617  ⊢  
  : , :
222instantiation584, 262, 467  ⊢  
  : , : , :
223instantiation263, 571, 264, 265, 266, 267*  ⊢  
  : , : , : , : , : , :
224instantiation584, 268, 467  ⊢  
  : , : , :
225instantiation584, 269, 467  ⊢  
  : , : , :
226instantiation270, 271, 579, 272*  ⊢  
  : , : , :
227instantiation422, 614, 273, 274, 425, 426  ⊢  
  : , : , : , :
228instantiation584, 275, 276  ⊢  
  : , : , :
229instantiation508, 277  ⊢  
  : , : , :
230instantiation678, 453, 656,  ⊢  
  : , :
231instantiation511, 278,  ⊢  
  : , :
232instantiation508, 358  ⊢  
  : , : , :
233instantiation510, 536  ⊢  
  : , :
234conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
235instantiation471, 654, 677, 279  ⊢  
  : , : , : , :
236generalization280  ⊢  
237axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
238conjecture  ⊢  
 proveit.core_expr_types.operations.operands_substitution_via_tuple
239instantiation584, 281, 467  ⊢  
  : , : , :
240instantiation282, 283, 284, 562*  ⊢  
  : , : , : , :
241instantiation285, 689  ⊢  
  :
242modus ponens286, 287  ⊢  
243instantiation632  ⊢  
  : , : , :
244instantiation632  ⊢  
  : , : , :
245conjecture  ⊢  
 proveit.physics.quantum.circuits.unary_multi_output_reduction
246instantiation367, 633, 368, 288, 289, 371*,  ⊢  
  : , : , :
247instantiation685, 655, 290,  ⊢  
  : , : , :
248instantiation584, 291, 292  ⊢  
  : , : , :
249instantiation584, 293, 294  ⊢  
  : , : , :
250instantiation685, 672, 295,  ⊢  
  : , : , :
251instantiation673, 676, 677, 295,  ⊢  
  : , : , :
252instantiation685, 551, 296  ⊢  
  : , : , :
253instantiation514, 533, 515, 297,  ⊢  
  : , : , : , :
254instantiation298, 602  ⊢  
  :
255instantiation422, 614, 299, 300, 425, 528  ⊢  
  : , : , : , :
256instantiation584, 301, 302  ⊢  
  : , : , :
257instantiation526, 303, 304  ⊢  
  : , : , :
258instantiation631  ⊢  
  : , :
259instantiation576, 407  ⊢  
  : , : , :
260instantiation584, 305, 306  ⊢  
  : , : , :
261conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
262instantiation578, 307, 528  ⊢  
  : , : , :
263conjecture  ⊢  
 proveit.core_expr_types.tuples.shift_equivalence
264instantiation526, 527, 308  ⊢  
  : , : , :
265instantiation492, 309  ⊢  
  : , :
266instantiation492, 310  ⊢  
  : , :
267instantiation609, 682, 664, 610, 615, 311, 312, 618, 617,  ⊢  
  : , : , : , : , : , :
268instantiation578, 313, 401  ⊢  
  : , : , :
269instantiation314, 315, 316*  ⊢  
  : , : , : , :
270conjecture  ⊢  
 proveit.core_expr_types.tuples.partition_back
271instantiation526, 317, 318  ⊢  
  : , : , :
272instantiation319, 619, 617  ⊢  
  : , :
273instantiation632  ⊢  
  : , : , :
274instantiation632  ⊢  
  : , : , :
275instantiation609, 610, 664, 611, 619, 617, 618  ⊢  
  : , : , : , : , : , :
276instantiation320, 682, 610, 615, 619, 617  ⊢  
  : , : , : , : , : , : , :
277instantiation526, 321, 322  ⊢  
  : , : , :
278instantiation323, 324, 325,  ⊢  
  : , : , :
279instantiation526, 326, 605  ⊢  
  : , : , :
280instantiation492, 327,  ⊢  
  : , :
281instantiation328, 666, 329, 330, 344, 331, 358, 332*  ⊢  
  : , : , : , :
282conjecture  ⊢  
 proveit.core_expr_types.tuples.merge_front
283instantiation526, 536, 333  ⊢  
  : , : , :
284instantiation492, 353  ⊢  
  : , :
285axiom  ⊢  
 proveit.physics.quantum.QPE._psi_t_def
286instantiation334, 682, 509, 610, 335, 615, 528, 385  ⊢  
  : , : , : , : , : , : , : , :
287instantiation384, 666, 381, 382, 383, 336, 337, 338  ⊢  
  : , : , : , :
288instantiation685, 652, 339,  ⊢  
  : , : , :
289instantiation410, 676, 677, 674,  ⊢  
  : , : , :
290instantiation685, 340, 341,  ⊢  
  : , : , :
291instantiation576, 407  ⊢  
  : , : , :
292instantiation540, 682, 664, 610, 615, 342, 602, 612, 619, 343*  ⊢  
  : , : , : , : , : , :
293instantiation576, 407  ⊢  
  : , : , :
294instantiation540, 682, 664, 610, 615, 344, 619, 612, 345*  ⊢  
  : , : , : , : , : , :
295assumption  ⊢  
296instantiation568, 569, 346  ⊢  
  : , :
297instantiation532, 533, 347, 535,  ⊢  
  : , : , : , :
298conjecture  ⊢  
 proveit.numbers.exponentiation.complex_x_to_first_power_is_x
299instantiation632  ⊢  
  : , : , :
300instantiation632  ⊢  
  : , : , :
301instantiation558, 610, 682, 615, 619, 617  ⊢  
  : , : , : , : , : , : , :
302instantiation540, 682, 664, 610, 615, 445, 619, 617, 603*  ⊢  
  : , : , : , : , : , :
303instantiation685, 543, 348  ⊢  
  : , : , :
304instantiation584, 349, 350  ⊢  
  : , : , :
305instantiation609, 682, 664, 610, 615, 477, 617, 619, 612  ⊢  
  : , : , : , : , : , :
306instantiation613, 664, 682, 477, 615, 617, 619  ⊢  
  : , : , : , :
307instantiation508, 509  ⊢  
  : , : , :
308instantiation584, 351, 378  ⊢  
  : , : , :
309instantiation584, 352, 353  ⊢  
  : , : , :
310instantiation584, 354, 605  ⊢  
  : , : , :
311instantiation631  ⊢  
  : , :
312instantiation685, 635, 355,  ⊢  
  : , : , :
313instantiation508, 356  ⊢  
  : , : , :
314conjecture  ⊢  
 proveit.core_expr_types.tuples.extended_range_len
315instantiation357, 358  ⊢  
  : , : , :
316instantiation584, 359, 360  ⊢  
  : , : , :
317instantiation578, 536, 361  ⊢  
  : , : , :
318instantiation584, 362, 363  ⊢  
  : , : , :
319conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_12
320conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general
321instantiation685, 543, 364  ⊢  
  : , : , :
322instantiation584, 365, 366  ⊢  
  : , : , :
323conjecture  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
324conjecture  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
325instantiation367, 633, 368, 369, 370, 371*,  ⊢  
  : , : , :
326instantiation372, 607, 634, 630, 373, 374*  ⊢  
  : , : , :
327instantiation584, 375, 376,  ⊢  
  : , : , :
328conjecture  ⊢  
 proveit.core_expr_types.tuples.general_len
329instantiation631  ⊢  
  : , :
330instantiation631  ⊢  
  : , :
331instantiation526, 610, 425  ⊢  
  : , : , :
332instantiation584, 377, 378  ⊢  
  : , : , :
333instantiation584, 379, 380  ⊢  
  : , : , :
334conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_disassociation
335instantiation431, 666, 381, 382, 383  ⊢  
  : , : , :
336instantiation631  ⊢  
  : , :
337instantiation384, 432, 528, 433, 434, 385, 386  ⊢  
  : , : , : , :
338axiom  ⊢  
 proveit.physics.quantum.QPE._u_ket_register
339instantiation685, 655, 670,  ⊢  
  : , : , :
340instantiation675, 680, 656  ⊢  
  : , :
341assumption  ⊢  
342instantiation631  ⊢  
  : , :
343instantiation584, 387, 388  ⊢  
  : , : , :
344instantiation631  ⊢  
  : , :
345instantiation584, 389, 603  ⊢  
  : , : , :
346instantiation591, 592, 390, 602, 594, 595, 391, 597  ⊢  
  : , :
347instantiation685, 551, 392,  ⊢  
  : , : , :
348instantiation406, 689, 666  ⊢  
  : , :
349instantiation576, 407  ⊢  
  : , : , :
350instantiation584, 393, 394  ⊢  
  : , : , :
351instantiation584, 395, 396  ⊢  
  : , : , :
352instantiation576, 399  ⊢  
  : , : , :
353instantiation584, 397, 398  ⊢  
  : , : , :
354instantiation576, 399  ⊢  
  : , : , :
355instantiation685, 652, 400,  ⊢  
  : , : , :
356instantiation526, 527, 401  ⊢  
  : , : , :
357conjecture  ⊢  
 proveit.core_expr_types.tuples.range_len_is_nat
358instantiation526, 536, 426  ⊢  
  : , : , :
359instantiation576, 488  ⊢  
  : , : , :
360instantiation584, 402, 403  ⊢  
  : , : , :
361instantiation606, 617, 618  ⊢  
  : , :
362instantiation576, 488  ⊢  
  : , : , :
363instantiation584, 404, 405  ⊢  
  : , : , :
364instantiation406, 689, 687  ⊢  
  : , :
365instantiation576, 407  ⊢  
  : , : , :
366instantiation613, 610, 617, 619  ⊢  
  : , : , : , :
367conjecture  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
368instantiation685, 652, 408  ⊢  
  : , : , :
369instantiation685, 652, 409,  ⊢  
  : , : , :
370instantiation410, 676, 677, 483,  ⊢  
  : , : , :
371instantiation584, 411, 412  ⊢  
  : , : , :
372conjecture  ⊢  
 proveit.numbers.ordering.less_eq_shift_add_right
373instantiation413, 634, 649, 633, 573, 414, 415*, 416*  ⊢  
  : , : , :
374instantiation578, 417, 418  ⊢  
  : , : , :
375instantiation609, 682, 614, 610, 615, 419, 421, 618, 617, 619,  ⊢  
  : , : , : , : , : , :
376instantiation420, 610, 682, 615, 421, 619, 617,  ⊢  
  : , : , : , : , : , : , :
377instantiation422, 664, 423, 424, 425, 426  ⊢  
  : , : , : , :
378instantiation584, 427, 428  ⊢  
  : , : , :
379instantiation576, 562  ⊢  
  : , : , :
380instantiation584, 429, 430  ⊢  
  : , : , :
381instantiation631  ⊢  
  : , :
382instantiation431, 432, 528, 433, 434  ⊢  
  : , : , :
383instantiation550, 435  ⊢  
  :
384conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space
385instantiation584, 436, 467  ⊢  
  : , : , :
386modus ponens437, 438  ⊢  
387instantiation576, 439  ⊢  
  : , : , :
388conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_2_1
389instantiation576, 440  ⊢  
  : , : , :
390instantiation624  ⊢  
  : , : , : , : , :
391instantiation685, 635, 441  ⊢  
  : , : , :
392instantiation568, 569, 442,  ⊢  
  : , :
393instantiation584, 443, 444  ⊢  
  : , : , :
394instantiation540, 610, 664, 682, 445, 615, 617, 619, 603*  ⊢  
  : , : , : , : , : , :
395instantiation576, 605  ⊢  
  : , : , :
396instantiation576, 562  ⊢  
  : , : , :
397instantiation609, 682, 664, 610, 615, 454, 582, 619  ⊢  
  : , : , : , : , : , :
398instantiation540, 610, 664, 682, 445, 615, 582, 619, 603*  ⊢  
  : , : , : , : , : , :
399instantiation608, 619  ⊢  
  :
400instantiation685, 655, 446,  ⊢  
  : , : , :
401instantiation584, 447, 448  ⊢  
  : , : , :
402instantiation584, 449, 450  ⊢  
  : , : , :
403instantiation587, 602, 617  ⊢  
  : , :
404instantiation584, 451, 452  ⊢  
  : , : , :
405instantiation540, 682, 664, 610, 615, 541, 619, 559, 617, 577*  ⊢  
  : , : , : , : , : , :
406conjecture  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
407conjecture  ⊢  
 proveit.numbers.negation.negated_zero
408instantiation685, 655, 676  ⊢  
  : , : , :
409instantiation685, 655, 453,  ⊢  
  : , : , :
410conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
411instantiation609, 682, 664, 610, 615, 454, 582, 619, 617  ⊢  
  : , : , : , : , : , :
412instantiation455, 617, 619  ⊢  
  : , :
413conjecture  ⊢  
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
414instantiation511, 456  ⊢  
  : , :
415instantiation458, 619, 617, 457*  ⊢  
  : , :
416instantiation458, 619, 459*  ⊢  
  : , :
417instantiation604, 619, 602, 603  ⊢  
  : , : , :
418instantiation606, 602, 618  ⊢  
  : , :
419instantiation632  ⊢  
  : , : , :
420conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_general_rev
421instantiation685, 635, 460,  ⊢  
  : , : , :
422axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
423instantiation631  ⊢  
  : , :
424instantiation631  ⊢  
  : , :
425instantiation540, 682, 664, 610, 615, 461, 619, 618, 462*  ⊢  
  : , : , : , : , : , :
426instantiation584, 463, 464  ⊢  
  : , : , :
427instantiation609, 610, 664, 682, 611, 615, 619, 617, 618  ⊢  
  : , : , : , : , : , :
428instantiation465, 619, 617  ⊢  
  : , :
429instantiation609, 610, 664, 682, 611, 615, 612, 617, 618  ⊢  
  : , : , : , : , : , :
430instantiation613, 682, 664, 615, 611, 617, 618  ⊢  
  : , : , : , :
431conjecture  ⊢  
 proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space
432instantiation526, 689, 528  ⊢  
  : , : , :
433instantiation584, 466, 467  ⊢  
  : , : , :
434instantiation468, 676, 677, 533, 472  ⊢  
  : , : , :
435instantiation663, 664, 469  ⊢  
  : , :
436instantiation578, 470, 528  ⊢  
  : , : , :
437instantiation471, 676, 677, 472  ⊢  
  : , : , : , :
438generalization473  ⊢  
439conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_2_0
440conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_0
441instantiation685, 652, 474  ⊢  
  : , : , :
442instantiation591, 592, 593, 602, 594, 595, 475, 597,  ⊢  
  : , :
443instantiation609, 682, 664, 615, 477, 476, 617, 619, 612  ⊢  
  : , : , : , : , : , :
444instantiation613, 664, 610, 477, 617, 619  ⊢  
  : , : , : , :
445instantiation631  ⊢  
  : , :
446instantiation685, 478, 479,  ⊢  
  : , : , :
447instantiation576, 488  ⊢  
  : , : , :
448instantiation584, 480, 481  ⊢  
  : , : , :
449instantiation609, 610, 664, 557, 612, 617, 559, 602  ⊢  
  : , : , : , : , : , :
450instantiation613, 682, 614, 615, 482, 617, 559, 602  ⊢  
  : , : , : , :
451instantiation609, 610, 664, 682, 557, 615, 619, 617, 559  ⊢  
  : , : , : , : , : , :
452instantiation558, 610, 682, 615, 619, 617, 559  ⊢  
  : , : , : , : , : , : , :
453instantiation685, 672, 483,  ⊢  
  : , : , :
454instantiation631  ⊢  
  : , :
455conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_31
456instantiation546, 598  ⊢  
  :
457instantiation484, 617  ⊢  
  :
458conjecture  ⊢  
 proveit.numbers.multiplication.mult_neg_left
459instantiation485, 619  ⊢  
  :
460instantiation685, 652, 486,  ⊢  
  : , : , :
461instantiation631  ⊢  
  : , :
462instantiation584, 487, 605  ⊢  
  : , : , :
463instantiation576, 488  ⊢  
  : , : , :
464instantiation584, 489, 490  ⊢  
  : , : , :
465conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_13
466instantiation578, 491, 528  ⊢  
  : , : , :
467instantiation492, 493  ⊢  
  : , :
468conjecture  ⊢  
 proveit.logic.booleans.conjunction.redundant_conjunction_general
469instantiation685, 543, 494  ⊢  
  : , : , :
470instantiation508, 509  ⊢  
  : , : , :
471conjecture  ⊢  
 proveit.logic.booleans.conjunction.conjunction_from_quantification
472instantiation526, 495, 605  ⊢  
  : , : , :
473instantiation532, 533, 496, 497,  ⊢  
  : , : , : , :
474instantiation685, 655, 498  ⊢  
  : , : , :
475instantiation685, 635, 499,  ⊢  
  : , : , :
476instantiation631  ⊢  
  : , :
477instantiation631  ⊢  
  : , :
478instantiation675, 654, 680  ⊢  
  : , :
479assumption  ⊢  
480instantiation584, 500, 501  ⊢  
  : , : , :
481instantiation502, 617  ⊢  
  :
482instantiation632  ⊢  
  : , : , :
483assumption  ⊢  
484conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_left
485conjecture  ⊢  
 proveit.numbers.multiplication.elim_one_right
486instantiation685, 655, 503,  ⊢  
  : , : , :
487instantiation576, 579  ⊢  
  : , : , :
488instantiation581, 582, 602, 583*  ⊢  
  : , :
489instantiation584, 504, 505  ⊢  
  : , : , :
490instantiation540, 610, 664, 682, 506, 615, 617, 559, 619, 507*  ⊢  
  : , : , : , : , : , :
491instantiation508, 509  ⊢  
  : , : , :
492theorem  ⊢  
 proveit.logic.equality.equals_reversal
493instantiation510, 527  ⊢  
  : , :
494axiom  ⊢  
 proveit.physics.quantum.QPE._s_in_nat_pos
495instantiation511, 512  ⊢  
  : , :
496instantiation685, 635, 513  ⊢  
  : , : , :
497instantiation514, 533, 515, 516,  ⊢  
  : , : , : , :
498instantiation685, 686, 517  ⊢  
  : , : , :
499instantiation685, 652, 518,  ⊢  
  : , : , :
500instantiation584, 519, 520  ⊢  
  : , : , :
501instantiation540, 682, 614, 610, 615, 521, 619, 559, 617, 522*  ⊢  
  : , : , : , : , : , :
502conjecture  ⊢  
 proveit.numbers.addition.elim_zero_left
503instantiation685, 644, 523,  ⊢  
  : , : , :
504instantiation609, 610, 664, 557, 612, 617, 559, 619  ⊢  
  : , : , : , : , : , :
505instantiation613, 682, 614, 615, 524, 617, 559, 619  ⊢  
  : , : , : , :
506instantiation631  ⊢  
  : , :
507instantiation578, 577, 525  ⊢  
  : , : , :
508conjecture  ⊢  
 proveit.core_expr_types.tuples.range_len
509instantiation526, 527, 528  ⊢  
  : , : , :
510conjecture  ⊢  
 proveit.core_expr_types.tuples.range_from1_len
511conjecture  ⊢  
 proveit.numbers.ordering.relax_less
512instantiation529, 607, 642, 649, 530, 605*  ⊢  
  : , : , :
513instantiation685, 638, 531  ⊢  
  : , : , :
514conjecture  ⊢  
 proveit.linear_algebra.addition.binary_closure
515conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_zero_in_qubit_space
516instantiation532, 533, 534, 535,  ⊢  
  : , : , : , :
517instantiation663, 664, 536  ⊢  
  : , :
518instantiation685, 655, 537,  ⊢  
  : , : , :
519instantiation584, 538, 539  ⊢  
  : , : , :
520instantiation558, 664, 610, 682, 541, 615, 619, 559, 617  ⊢  
  : , : , : , : , : , : , :
521instantiation632  ⊢  
  : , : , :
522instantiation540, 682, 664, 610, 615, 541, 619, 559, 542*  ⊢  
  : , : , : , : , : , :
523assumption  ⊢  
524instantiation632  ⊢  
  : , : , :
525instantiation606, 619, 559  ⊢  
  : , :
526theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
527instantiation685, 543, 689  ⊢  
  : , : , :
528instantiation584, 544, 545  ⊢  
  : , : , :
529conjecture  ⊢  
 proveit.numbers.ordering.less_shift_add_right
530instantiation546, 684  ⊢  
  :
531instantiation547, 548, 588, 549  ⊢  
  : , :
532conjecture  ⊢  
 proveit.linear_algebra.scalar_multiplication.scalar_mult_closure
533instantiation550, 666  ⊢  
  :
534instantiation685, 551, 552,  ⊢  
  : , : , :
535conjecture  ⊢  
 proveit.physics.quantum.algebra.ket_one_in_qubit_space
536instantiation553, 554, 555  ⊢  
  :
537instantiation685, 686, 556,  ⊢  
  : , : , :
538instantiation609, 610, 664, 557, 619, 617, 559  ⊢  
  : , : , : , : , : , :
539instantiation558, 610, 619, 617, 559  ⊢  
  : , : , : , : , : , : , :
540conjecture  ⊢  
 proveit.numbers.addition.association
541instantiation631  ⊢  
  : , :
542instantiation584, 560, 561  ⊢  
  : , : , :
543conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
544instantiation576, 562  ⊢  
  : , : , :
545instantiation584, 563, 564  ⊢  
  : , : , :
546conjecture  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
547conjecture  ⊢  
 proveit.numbers.division.div_real_pos_closure
548instantiation685, 636, 565  ⊢  
  : , : , :
549instantiation566, 567  ⊢  
  :
550conjecture  ⊢  
 proveit.linear_algebra.complex_vec_set_is_vec_space
551conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.complex_nonzero_within_complex
552instantiation568, 569, 570,  ⊢  
  : , :
553conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
554instantiation678, 656, 571  ⊢  
  : , :
555instantiation572, 573  ⊢  
  : , :
556instantiation663, 664, 574,  ⊢  
  : , :
557instantiation631  ⊢  
  : , :
558conjecture  ⊢  
 proveit.numbers.addition.leftward_commutation
559instantiation685, 635, 575  ⊢  
  : , : , :
560instantiation576, 577  ⊢  
  : , : , :
561instantiation578, 579, 580  ⊢  
  : , : , :
562instantiation581, 582, 619, 583*  ⊢  
  : , :
563instantiation584, 585, 586  ⊢  
  : , : , :
564instantiation587, 619, 617  ⊢  
  : , :
565instantiation685, 650, 687  ⊢  
  : , : , :
566conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
567instantiation685, 622, 588  ⊢  
  : , : , :
568conjecture  ⊢  
 proveit.numbers.exponentiation.exp_complex_nonzero_closure
569instantiation685, 589, 590  ⊢  
  : , : , :
570instantiation591, 592, 593, 602, 594, 595, 596, 597,  ⊢  
  : , :
571instantiation685, 683, 598  ⊢  
  : , : , :
572conjecture  ⊢  
 proveit.numbers.addition.subtraction.nonneg_difference
573instantiation599, 689  ⊢  
  :
574instantiation667, 600,  ⊢  
  :
575instantiation648, 630  ⊢  
  :
576axiom  ⊢  
 proveit.logic.equality.substitution
577instantiation601, 619, 602, 603  ⊢  
  : , : , :
578theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
579instantiation604, 612, 619, 605  ⊢  
  : , : , :
580instantiation606, 619, 618  ⊢  
  : , :
581conjecture  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
582instantiation685, 635, 607  ⊢  
  : , : , :
583instantiation608, 617  ⊢  
  :
584axiom  ⊢  
 proveit.logic.equality.equals_transitivity
585instantiation609, 610, 664, 611, 612, 617, 618, 619  ⊢  
  : , : , : , : , : , :
586instantiation613, 682, 614, 615, 616, 617, 618, 619  ⊢  
  : , : , : , :
587conjecture  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_32
588instantiation620, 621  ⊢  
  :
589conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
590instantiation685, 622, 623  ⊢  
  : , : , :
591conjecture  ⊢  
 proveit.numbers.multiplication.mult_complex_closure
592conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat5
593instantiation624  ⊢  
  : , : , : , : , :
594instantiation685, 635, 625  ⊢  
  : , : , :
595conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
596instantiation685, 635, 626,  ⊢  
  : , : , :
597instantiation685, 635, 627  ⊢  
  : , : , :
598instantiation688, 687  ⊢  
  :
599conjecture  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
600instantiation669, 628, 629,  ⊢  
  :
601conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
602instantiation685, 635, 630  ⊢  
  : , : , :
603conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
604conjecture  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add
605conjecture  ⊢  
 proveit.numbers.numerals.decimals.add_0_1
606conjecture  ⊢  
 proveit.numbers.addition.commutation
607instantiation648, 633  ⊢  
  :
608conjecture  ⊢  
 proveit.numbers.negation.double_negation
609conjecture  ⊢  
 proveit.numbers.addition.disassociation
610theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
611instantiation631  ⊢  
  : , :
612instantiation685, 635, 642  ⊢  
  : , : , :
613conjecture  ⊢  
 proveit.numbers.addition.elim_zero_any
614conjecture  ⊢  
 proveit.numbers.numerals.decimals.nat3
615conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
616instantiation632  ⊢  
  : , : , :
617instantiation685, 635, 633  ⊢  
  : , : , :
618instantiation685, 635, 634  ⊢  
  : , : , :
619instantiation685, 635, 649  ⊢  
  : , : , :
620conjecture  ⊢  
 proveit.numbers.exponentiation.sqrt_real_pos_closure
621instantiation685, 636, 637  ⊢  
  : , : , :
622conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
623conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
624conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
625instantiation685, 638, 639  ⊢  
  : , : , :
626instantiation685, 652, 640,  ⊢  
  : , : , :
627instantiation641, 642, 649, 643  ⊢  
  : , : , :
628instantiation685, 644, 645,  ⊢  
  : , : , :
629instantiation673, 654, 677, 645,  ⊢  
  : , : , :
630instantiation685, 652, 646  ⊢  
  : , : , :
631conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
632conjecture  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
633instantiation685, 652, 647  ⊢  
  : , : , :
634instantiation648, 649  ⊢  
  :
635conjecture  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
636conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
637instantiation685, 650, 666  ⊢  
  : , : , :
638conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
639conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
640instantiation685, 655, 651,  ⊢  
  : , : , :
641conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
642instantiation685, 652, 653  ⊢  
  : , : , :
643axiom  ⊢  
 proveit.physics.quantum.QPE._phase_in_interval
644instantiation675, 654, 677  ⊢  
  : , :
645assumption  ⊢  
646instantiation685, 655, 660  ⊢  
  : , : , :
647instantiation685, 655, 656  ⊢  
  : , : , :
648conjecture  ⊢  
 proveit.numbers.negation.real_closure
649instantiation657, 658, 687  ⊢  
  : , : , :
650conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
651instantiation685, 686, 659,  ⊢  
  : , : , :
652conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
653conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.zero_is_rational
654instantiation678, 679, 660  ⊢  
  : , :
655conjecture  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
656instantiation685, 686, 689  ⊢  
  : , : , :
657theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
658instantiation661, 662  ⊢  
  : , :
659instantiation663, 664, 665,  ⊢  
  : , :
660instantiation685, 686, 666  ⊢  
  : , : , :
661theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
662conjecture  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
663conjecture  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
664theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
665instantiation667, 668,  ⊢  
  :
666conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat2
667conjecture  ⊢  
 proveit.numbers.negation.nat_closure
668instantiation669, 670, 671,  ⊢  
  :
669conjecture  ⊢  
 proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos
670instantiation685, 672, 674,  ⊢  
  : , : , :
671instantiation673, 676, 677, 674,  ⊢  
  : , : , :
672instantiation675, 676, 677  ⊢  
  : , :
673conjecture  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
674assumption  ⊢  
675conjecture  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
676instantiation678, 679, 680  ⊢  
  : , :
677instantiation685, 681, 682  ⊢  
  : , : , :
678conjecture  ⊢  
 proveit.numbers.addition.add_int_closure_bin
679instantiation685, 683, 684  ⊢  
  : , : , :
680instantiation685, 686, 687  ⊢  
  : , : , :
681conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
682axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
683conjecture  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
684instantiation688, 689  ⊢  
  :
685theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
686conjecture  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
687conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat1
688conjecture  ⊢  
 proveit.numbers.negation.int_neg_closure
689assumption  ⊢  
*equality replacement requirements